\begin{tabbing}
sends{-}p(${\it es}$; ${\it ds}$; $k$; $T$; $l$; ${\it dt}$; $g$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; source($l$); $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))\+
\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; $e$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; $e$) = $l$ $\in$ IdLnk)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); fpf{-}cap(${\it dt}$; id{-}deq; es{-}tag(${\it es}$; $e$); top))))
\-\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]source($l$);
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}valtype(${\it es}$; $e$); $T$)\+
\\[0ex]c$\wedge$ ($\exists$\=$L$:\{\=$e$:es{-}E(${\it es}$)$\mid$ \+\+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; $e$))
\\[0ex]c$\wedge$ \=((es{-}lnk(${\it es}$; $e$) = $l$ $\in$ IdLnk)\+
\\[0ex]$\wedge$ ($\uparrow$fpf{-}dom(id{-}deq; es{-}tag(${\it es}$; $e$); ${\it dt}$)))\}  List
\-\-\\[0ex](es{-}rcv{-}from(${\it es}$; $e$; $l$; $L$)
\\[0ex]c$\wedge$ (\=map(($\lambda$$e$.$<$es{-}tag(${\it es}$; $e$), es{-}val(${\it es}$; $e$)$>$); $L$)\+
\\[0ex]=
\\[0ex]concat(map(\=($\lambda$${\it tgf}$.sends{-}msgs(\=es{-}state{-}when(${\it es}$; $e$);\+\+
\\[0ex]es{-}val(${\it es}$; $e$);
\\[0ex]${\it tgf}$));
\-\\[0ex]$g$))
\-\\[0ex]$\in$ ((${\it tg}$:Id $\times$ fpf{-}cap(${\it dt}$; id{-}deq; ${\it tg}$; void)) List)))))))
\-\-\-\-\-
\end{tabbing}